$\forall$${\it es}$:ES, $P$:(E$\rightarrow\mathbb{P}$), $e$:E. ($\forall$$e$:E. Dec($P$($e$))) $\Rightarrow$ Dec($\exists$$a$:E. (es{-}p{-}le{-}pred(${\it es}$;$P$)($e$,$a$)))